#!/usr/bin/env ruby

class String
    def begins?(s)
        self[0...(s.size)] == s
    end

    def ends?(s)
        self[(self.size - s.size)...(self.size)] == s
    end
end

REGULAR_ARGS = 2
BMC_ARGS = 4

STATES_EXTRACTOR = /number of reachable states = ([0-9\.e\+]+)/
MEMORY_EXTRACTOR = /BDD memory in use = ([0-9\.e\+]+)/
COUNT_EXTRACTOR = /([0-9\.e\+]+)/
NUMBER_EXTRACTOR = /([0-9\.]+)/

MCMAS_EXECUTABLE = "./../../mcmas"
#MODEL = "3_5_03.ispl"

if __FILE__ == $0 then

    i = 0
    model = ARGV[0]
    #puts model
    while true do
        #puts i
        output = `/usr/bin/time -p #{MCMAS_EXECUTABLE} -one_shot #{i} -e 6 #{model} 2>&1 3>&1 | tee "#{model}_#{i}.out"`
        cexline = `cat "#{model}_#{i}.out" | tail -n 11 | head -n 1`
        fpline = `cat "#{model}_#{i}.out" | tail -n 10 | head -n 1`

        cex = cexline.index("CEX found at")
       
        fix = fpline.index("Fix Point:")
        
        if (cex || fix) then
            #puts i
            temp=`cat "#{model}_#{i}.out" | tail -n 5 | head -n 2`
            puts temp
            break
        end
        
        i += 1
    end

end


